COMMENT ⊗   VALID 00002 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	% Prove rev1[u*v,w] = rev1[v,rev1[u,w]] which gives
C00003 ENDMK
C⊗;
% Prove rev1[u*v,w] = rev1[v,rev1[u,w]] which gives
% reverse[u*v] = reverse v * reverse u, a kind of distributivity

LABEL I_DIS;
∧I LISTINDUCTION1[PHI ← λu.(∀v w.(rev1(u*v,w) = rev1(v,rev1(u,w))))];

LABEL NIL_DIS;
EVAL ∀v w.(rev1(qNIL*v,w) = rev1(v,rev1(qNIL,w))) BY {APPEND_DEF,REV1_DEF};

LABEL H_DIS;
ASSUME I_DIS:#1#2#1#1;
REWRITE ∀v w.(rev1(uu*v,w) = rev1(v,rev1(uu,w))) BY LOGICTREE∪SEXPSS∪{H_DIS,
APPEND_DEF,REV1_DEF};

⊃I H_REV1⊃↑; ∀I ↑ uu;

TAUT I_DIS:#2 I_DIS,NIL_DIS,↑;
THEOREM DISTRIB_REVERSE ↑;